Nuprl Lemma : imin_lb
13,42
postcript
pdf
a
,
b
,
c
:
. (imin(
a
;
b
)
c
)
((
a
c
)
(
b
c
))
latex
Up
int
2
,
int
2
Definitions
True
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
a, b, c:
. (imin(a;b) 
c) 
((a c) 
(b c)) a, b, c:. (imin(a;b) c) ((a c) (b c)) Q Q Q Q
Tx:A. B(x)